#define N 2   
#define M 6    /* full password length */
#define max_loss 200
bit code[M]   
mtype = {ack};

proctype proc (byte my_id, next_id, previous_id; chan to_next, from_previous, to_receiver, send_receipt){
	bit my_code[M] ;
	byte i = 0;
	byte j = 0;
	byte k = 0;
	byte m = 0;
	byte n = 0;

/* declare more variables */

/* first getting the N bits belonging to this process from the global password */
	do
		:: i < N -> my_code[my_id*N+i] = code[my_id*N+i]; i++
		:: i == N -> break
	od;

/* now the communication and result calculation begins ... */
	do
		:: j < N -> to_next!my_code[my_id*N+j]->
			if
				:: (my_id == 1) ->
					from_previous?my_code[previous_id*N+j];
					send_receipt!ack;j++		
				:: (my_id == 0) ->
					do 
						:: send_receipt?ack -> from_previous?my_code[previous_id*N+j]; 
							j++;break
						:: timeout -> to_next!my_code[my_id*N+j]						
					od;
				:: (my_id == 2) ->
					from_previous?my_code[previous_id*N+j]; j++
			fi;
		:: j == N -> break	
	od;
	
/* Put the last 2 code in each Proc */
	do
		:: k < N -> to_next!my_code[previous_id*N+k];
			if
				:: (my_id == 1) ->
					from_previous?my_code[next_id*N+k];
					send_receipt!ack	;k++	
				:: (my_id == 0) ->
					do 
						:: send_receipt?ack -> from_previous?my_code[next_id*N+k]; 
							k++;break
						:: timeout -> to_next!my_code[previous_id*N+k]						
					od;
				:: (my_id == 2) ->
					from_previous?my_code[next_id*N+k]; k++
			fi;		
			/* from_previous?my_code[next_id*N+k]; k++ */
		:: k == N -> break
	od;


/* Save to Rcv */
	do
		:: m < M -> end1:to_receiver!my_code[m]; m++
		:: m == M -> break
	od	
}

proctype receiver (chan from_A, from_B, from_C){
	bit my_code[M];
	byte i = 0;
/* declare more variables */
/* now the communication and result calculation begins */
		if
			:: from_A?my_code[i]; i++ -> 
				do
					:: i < M -> from_A?my_code[i]; i++
					:: i == M -> break
				od;
			:: from_B?my_code[i]; i++ ->
				do
					:: i< M -> from_B?my_code[i];i++
					:: i == M -> break
				od;
			:: from_C?my_code[i]; i++ ->
				do
					:: i< M -> from_C?my_code[i];i++
					:: i == M -> break
				od;
		fi;
}

/* FAULTY CHANNEL */
proctype channel (chan in, out){
	byte d[1], lost = 0;
	end2:
		do
			:: in?d[0] -> if
							:: (lost <= max_loss) ->
								progress1: out!d[0]
							:: (lost < max_loss) -> lost ++
						  fi
		od
}
 
init { 
     chan  AtoB =  [2] of { bit };     /*message types for the channels may be extended in your solution !!! */
     chan  BtoC =  [2] of { bit }; 
     chan  CtoA =  [2] of { bit }; 
     chan  AtoR =  [2] of { bit }; 
     chan  BtoR =  [2] of { bit }; 
     chan  CtoR =  [2] of { bit };
     /* init FAULTY CHANNELS */ 
     chan  AtoF =  [1] of { bit };
     chan  FtoB =  [1] of { bit };
     /* init a channel for RECEIPT */
     chan  BtoA =  [0] of { mtype };

	atomic{
		code[0] = 1; 
      	code[1] = 0;
      	code[2] = 1; 
      	code[3] = 1;
      	code[4] = 1; 
      	code[5] = 0;

     	run proc (0,1,2,AtoF,CtoA,AtoR,BtoA);
     	run proc (1,2,0,BtoC,FtoB,BtoR,BtoA);
     	run proc (2,0,1,CtoA,BtoC,CtoR,BtoA);
     	run channel (AtoF, FtoB);
     	run receiver(AtoR,BtoR,CtoR);
	}
}